i, j:. (i  j )  ((-i)  (-j)) 

latex

ProofTree

Definitions	t  T, P  Q, P  Q, P & Q, P  Q, x:A. B(x),
Lemmas	le wf, ge wf